package plus;

public class S_Function extends Solution {
	public Type[] domain;
	public Type range;
	
	public S_Function(int arity) { this(Type.fresh_vars(arity), Type.variable()); }
	public S_Function(Type[] domain) { this(domain, Type.variable()); }
	public S_Function() { this(null, Type.variable()); }
	public S_Function(Type[] domain, Type range) {
		assert domainIsValid(domain);
		assert range != null;
		this.domain = domain;
		this.range = range;
	}
	
	private static boolean domainIsValid(Type[] domain) {
		if (domain != null) for (Type t:domain) assert t!=null;
		return true;
	}
	@Override
	public void conform_to(Solution _that, Gamma gamma) {
		S_Function that = (S_Function)_that;
		if (that.domain != null) {
			if (this.domain == null) this.domain = Type.fresh_vars(that.domain.length);
			if (domain.length == that.domain.length) Type.conform(domain, that.domain, gamma);
			else Type.mismatch(this.toString(), that.toString());
		}
		range.conform_to(that.range, gamma);
	}
	@Override public void unify_with(Solution _that) {
		S_Function that = (S_Function)_that;
		if (that.domain != null) {
			if (domain == null) { domain = that.domain; Uni.progress = true; }
			else if (domain.length != that.domain.length) Type.mismatch(this.toString(), that.toString());
			Type.unify(domain, that.domain);
		}
		range = that.range = Type.unify(range, that.range);
	}
	@Override Solution copy() {
		S_Function copy = new S_Function();
		if (domain != null) copy.domain = Type.fresh_vars(domain.length);
		return copy;
	}
	@Override Type subst(Type[] actuals) {
		S_Function copy = new S_Function();
		if (range != null) copy.range = range.chase().subst(actuals);
		if (domain != null) copy.domain = Type.subst(domain, actuals);
		return Type.fresh(copy);
	}
	@Override boolean isNullable() { return false; }
	@Override public boolean canConform(Solution that, Hypo h) {
		assert that != null ;
		S_Function s = (S_Function) that;
		if (!Type.canConform(range, s.range, h)) return false;
		if (null == domain) return true;
		if (null == s.domain) return true;
		return Type.canConform(domain, s.domain, h);
	}
	public boolean isVoid() { return range.chase() == B._void; }
}
